Nuprl Lemma : simplify-equal-imp
0,22
postcript
pdf
T
:Type,
x
,
y
,
z
:
T
.
y
=
z
((
x
=
y
x
=
z
)
x
=
y
)
latex
Definitions
P
Q
,
False
,
A
,
t
T
,
Prop
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
P
Q
Lemmas
not
wf
origin
T:Type, x, y, z:T. 
y = z 
((x = y x = z) 
x = y) T:Type, x, y, z:T. y = z ((x = y x = z) x = y) QA
Tx:A. B(x) Q Q